es:event_system{i:l}, e:es-E(es), l:IdLnk, L:(es-E(es) List).
es-rcv-from(es; e; l; L)  (es-receives(es; e; l) = L) 

latex

Definitions	t  T, x:A. B(x), P  Q, A c B, x:A  B(x), x:AB(x), P  Q, P  Q, es-lnk(es; e), IdLnk, s = t, es-sender(es; e), es-E(es), es-isrcv(es; e), b, Type, prop{i:l}, (x  l), P  Q, es-receives(es; e; l), l-ordered(T; x,y.R(x;y); L), loc-ordered(es; L), es-rcv-from(es; e; l; L), event_system{i:l}, type List
Lemmas	es-rcv-from wf, event system wf, loc-ordered-equality, iff functionality wrt iff, member-es-receives, es-receives wf, l member wf, assert wf, es-isrcv wf, es-E wf, es-sender wf, IdLnk wf, es-lnk wf, loc-ordered-es-receives